Nuprl Definition : comm
13,42
postcript
pdf
basic
Comm(
T
;
op
) ==
x
,
y
:
T
. (
x
op
y
) = (
y
op
x
)
latex
clarification:
basic
Comm(
T
;
op
) ==
x
:
T
,
y
:
T
. (
x
op
y
) = (
y
op
x
)
T
latex
Up
gen
algebra
1
Wellformedness Lemmas
comm
wf
Definitions
x
:
A
.
B
(
x
)
,
x
f
y
origin
x, y:T. (x op y) = (y op x)
x:T, y:T. (x op y) = (y op x) 
T x, y:T. (x op y) = (y op x)
x:T, y:T. (x op y) = (y op x) T x:A. B(x)